perm filename PROVIN[E84,JMC]1 blob
sn#767898 filedate 1984-09-10 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00004 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 provin[e84,jmc] Draft of chapter 3 based on EKL
C00010 00003 1. (DECL CAR (UNARYNAME: CAR) (TYPE: |GROUND→GROUND|) (SYNTYPE: CONSTANT)
C00020 00004 (show)
C00021 ENDMK
C⊗;
provin[e84,jmc] Draft of chapter 3 based on EKL
In the part of this course concerned with proving properties of
programs we will use of the interactive theorem prover EKL
developed by Jussi Ketonen of Stanford University.
Its basic idea is a pure \lisp\ program can be directly
converted into a logical equation that can be used to prove
program properties. We begin with the example of our old friend
$append$ or $*$ treated informally. The program is
%
$$u*v ← \qif \qn u \qthen v \qelse \qa u\qcons[\qd u * v].$$
%
What might we want to prove about it?
Regarded as an operation on lists $append$ has
satisfies some algebraic equations. When we combine it with $reverse$,
which is also an operation on lists, we get a few more
equations. Here are the ones we'll prove.
%
$$\qNil * u = u$$
%
$$\u * \qNil = u$$
%
$$\u * [v * w] = [u*v]*w\hbox{\qquad \rm Associativity}$$
%
$$reverse reverse u = u$$
%
$$reverse[u*v] = reverse v * reverse u.$$
Each of these is true for all lists $u$ and $v$. We will see
that the first is trivial to prove, because it just involves substituting
in the definition of $append$, but each of the others involves a mathematical
induction. The main problem of this theory and the main technique the
user has to learn is that of setting up the mathematical inductions
needed to prove the theorems.
The first step is the replacement of the program by an
equation. In the case of $append$ the equation is
%
$$∀u v.u*v = \qif \qn u \qthen v \qelse \qa u\qcons[\qd u * v].$$
%
There are only two changes from the program. The first is
being explicit about the {\it quantifier} and is easy. $∀u v.$ in
front of the equation means that it is asserted to be true for
all lists $u$ and $v$ assuming our convention that the $u$ and
$v$ are variables that range of lists only. The second change is the
replacement of $←$ by $=$ and is more significant. $←$ identifies
a computer program. It says that to get the value of $u*v$
for particular values of $u$ and $v$ one substitutes these values
for the occurrences of $u$ and $v$ on the right side of the equation
and evaluates that right side. Recursion tells us how to deal
with occurrences of $*$ on the right side.
Replacing $←$ by equality means that there is some function
$λu v.u*v$ that is computed by this process, and it satisfies the
equation. This may seem obvious, but it isn't. The difficulties
are associated with the possibility that the recursive process
doesn't terminate. There is no way to restrict ourselves to
programs guaranteed to always terminate without eliminating
certain important and useful programs such as $eval$.
In this book we deal with the problem in two ways.
The first is that we have a number of recursion schemes such
as simple list and S-expression recursion that are guaranteed
to terminate. As part of the process of defining the equation
associated with he program, we prove that the recursion always
terminates. The second is that even without a guarantee of
termination there is still a sense in which the equation is
true. In fact the equation is true even if the program
never terminates. As mentioned in \chapref{readin} this is
accomplished by introducing the bottom symbol $\bot$, which
is taken as the value of the function defined by the program
when the program doesn't terminate.
EKL is a moderately powerful theorem prover, although
you have to tell it what inductions to do. However, its
performance is spotty. Sometimes it does the whole job in
one easy shot and other times it takes quite a bit of experiment
to make it do the right thing. Proving the associativity of
$append$ is one of the things EKL does easily, partly because
it was one of the examples used in developing EKL. Even
apart from that, the associativity of $append$ is really
straightforward. Here is the EKL proof.
EKL must be given a set of basic axioms for \lisp. We'll
go over them later, but for now assume it has been done.
The first thing to do is to define $append$. In order to use
the infix notation $u*v$, it is necessary to tell EKL about
the infix and its precedence rules, e.g. that let it know
that $\qd u * v$ is interpreted as $append[cdr[u],v]$. For
now we'll assume that this has been done. Moreover, EKL,
unlike \lisp\ external notation uses parentheses for grouping
and applying functions to arguments. Treating constant S-expressions
will have to be done by quoting.
(proof append)
(get-proofs lispax prf prf jk)
(show)
1. (DECL CAR (UNARYNAME: CAR) (TYPE: |GROUND→GROUND|) (SYNTYPE: CONSTANT)
(BINDINGPOWER: 950))
2. (DECL CDR (UNARYNAME: CDR) (TYPE: |GROUND→GROUND|) (SYNTYPE: CONSTANT)
(BINDINGPOWER: 950))
3. (DECL ATOM (UNARYNAME: ATOM) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
(BINDINGPOWER: 750))
4. (DECL NULL (UNARYNAME: NULL) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
(BINDINGPOWER: 750))
5. (DECL LISTP (UNARYNAME: LISTP) (TYPE: |GROUND→TRUTHVAL|)
(SYNTYPE: CONSTANT) (BINDINGPOWER: 750))
6. (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: |GROUND→TRUTHVAL|)
(SYNTYPE: CONSTANT) (BINDINGPOWER: 750))
7. (DECL SEXP (UNARYNAME: SEXP) (TYPE: |GROUND→TRUTHVAL|) (SYNTYPE: CONSTANT)
(BINDINGPOWER: 750))
8. (DECL (U V W) (TYPE: |GROUND|) (SORT: |LISTP|))
9. (DECL (X Y Z) (TYPE: |GROUND|) (SORT: |SEXP|))
10. (DECL (XA YA ZA) (TYPE: |GROUND|) (SORT: |ATOM|))
11. (DECL (PHI) (TYPE: |GROUND→TRUTHVAL|))
12. (DECL CONS (TYPE: |(GROUND⊗GROUND)→GROUND|) (SYNTYPE: CONSTANT)
(INFIXNAME: .) (PREFIXNAME: CONS) (BINDINGPOWER: 850))
;labels: SIMPINFO
13. (AXIOM |∀XA.SEXP XA|)
;labels: SIMPINFO
14. (AXIOM |∀U.SEXP U|)
;labels: SIMPINFO
15. (AXIOM |∀X U.LISTP X.U|)
;labels: SIMPINFO
16. (AXIOM |∀U.¬NULL U⊃LISTP CDR U|)
;labels: SIMPINFO
17. (AXIOM |∀U.¬NULL U⊃SEXP CAR U|)
;labels: SIMPINFO
18. (AXIOM |∀X.¬ATOM X⊃SEXP CAR X|)
;labels: SIMPINFO
19. (AXIOM |∀X.¬ATOM X⊃SEXP CDR X|)
;labels: SIMPINFO
20. (AXIOM |∀X Y.SEXP X.Y|)
;labels: SIMPINFO
21. (AXIOM |∀X Y.¬ATOM X.Y|)
;labels: SIMPINFO
22. (AXIOM |∀X U.¬NULL X.U|)
;labels: SIMPINFO
23. (AXIOM |∀U.NULL U⊃U=NIL|)
;labels: SIMPINFO
24. (AXIOM |∀X Y.CAR (X.Y)=X|)
;labels: SIMPINFO
25. (AXIOM |∀X Y.CDR (X.Y)=Y|)
;labels: SIMPINFO CONS_CAR_CDR
26. (AXIOM |∀U.¬NULL U⊃CAR U.CDR U=U|)
;labels: SIMPINFO CONS_CAR_CDR
27. (AXIOM |∀X.¬ATOM X⊃CAR X.CDR X=X|)
;labels: LISTINDUCTION
28. (AXIOM |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)
29. (DECL PARS (TYPE: |GROUND*|))
30. (DECL (DF DF1 DF2) (TYPE: |(GROUND⊗(GROUND*))→(GROUND*)|))
31. (DECL NILCASE (TYPE: |(GROUND*)→(GROUND*)|))
;labels: LISTINDUCTIONDEF
32. (AXIOM
|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧
FUN(X.U,PARS)=
DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)
;labels: SEXPINDUCTION
33. (AXIOM
|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)
;labels: SEXPINDUCTIONDEF
34. (AXIOM
|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃
FUN(Z,PARS)=
ATOMCASE(Z,PARS))∧
FUN(X.Y,PARS)=
DEFSEXP(X,Y,
FUN(X,
DF1(X,Y,
PARS)),
FUN(Y,
DF2(X,Y,
PARS)),
PARS)))|)
35. (DECL (ARB ARB1 ARB2) (TYPE: |?ARBITRARY|))
36. (DECL BIGFUN (TYPE: |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))
37. (DECL (DEFINED_FUN ATOM_FUN) (TYPE: |GROUND→(@ARB)|))
;labels: HIGH_ORDER_DEFINITION
38. (AXIOM
|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃
DEFINED_FUN(X)=ATOM_FUN(X))∧
DEFINED_FUN(X.Y)=
BIGFUN(X,Y,DEFINED_FUN(X),
DEFINED_FUN(Y))))|)
39. (DECL LIST (TYPE: |(GROUND*)→GROUND|) (SYNTYPE: CONSTANT))
40. (DECL LST (TYPE: |GROUND*|))
;labels: SIMPINFO
41. (AXIOM |LIST(())=NIL|)
;labels: SIMPINFO
42. (AXIOM |∀LST.LISTP LIST(LST)|)
;labels: SIMPINFO LISTDEF
43. (AXIOM |∀X LST.LIST(X,LST)=X.LIST(LST)|)
44. (DECL APPEND (TYPE: |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)
(SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *)
(BINDINGPOWER: 840))
;labels: SIMPINFO APPENDEF
45. (DEFAX APPEND |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)
;labels: SIMPINFO LISTAPPEND
46. (AXIOM |∀U V.LISTP U*V|)
;labels: SIMPINFO
47. (AXIOM |∀U.U*NIL=U|)
;labels: SIMPINFO
48. (AXIOM |∀X V.X.NIL*V=X.V|)
49. (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: |((@PHI)⊗GROUND)→TRUTHVAL|))
;labels: ALLPDEF
50. (DEFAX ALLP
|∀PHI X U.ALLP(PHI,NIL)∧
ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)
;labels: SOMEPDEF
51. (DEFAX SOMEP
|∀PHI X U.¬SOMEP(PHI,NIL)∧
SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)
;labels: MAPCARDEF
52. (DEFAX MAPCAR
|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)
53. (DECL (ALIST) (TYPE: |GROUND|) (SORT: |ALISTP|))
;labels: SIMPINFO
54. (AXIOM |∀ALIST.LISTP ALIST|)
;labels: ALISTDEF
55. (AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)
;labels: MKALIST
56. (AXIOM |∀XA Y ALIST.ALISTP (XA.Y).ALIST|)
57. (DECL ASSOC (TYPE: |(GROUND⊗GROUND)→GROUND|) (SYNTYPE: CONSTANT))
;labels: ASSOCDEF
58. (DEFAX ASSOC
|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧
ASSOC(X,(XA.Y).ALIST)=
(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)
;labels: SIMPINFO
59. (AXIOM |∀X ALIST.SEXP ASSOC(X,ALIST)|)
60. (DECL MEMBER (TYPE: |(GROUND⊗GROUND)→TRUTHVAL|) (SYNTYPE: CONSTANT))
;labels: MEMBERDEF
61. (DEFAX MEMBER |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)
62.
(show)